;; The first four lines of this file were added by Dracula.
;; They tell DrScheme that this is a Dracula Modular ACL2 program.
;; Leave these lines unchanged so that DrScheme can properly load this file.
#reader(planet "reader.rkt" ("cce" "dracula.plt") "modular" "lang")
(require "mcrop.lisp")
(require "mbmptree.lisp")
(require "mdatagenerators.lisp")

(module Tcrop
  (import Icrop)
  (import Ibmptree)
  (import IDataGenerators)
  
  (include-book "testing" :dir :teachpacks)
  (include-book "doublecheck" :dir :teachpacks)

  ; Generates a random pixel (random RGB values).
  (defrandom random-pixel ()
    (let* ((r (random-between 0 255))
           (g (random-between 0 255))
           (b (random-between 0 255)))
      (list r g b)))
  
  ; Random bitmap file, uses a static header with a 
  ; size of heightxwidth.
  (defrandom random-bitmap (height width)
    (let* ((header (list 66 77 54 12 0 0 0 0 0 0 54 0 0 
                         0 40 0 0 0 width 0 0 0 height 0 0 0 1 
                         0 24 0 0 0 0 0 0 12 0 0 0 0 0 
                         0 0 0 0 0 0 0 0 0 0 0 0 0))
           (pixels (random-list-of (random-pixel) 
                                   :size (* width height)))
           (tr (insert-header (empty-bmp-tree) header)))
      (fill-bitmap tr 0 0 height width pixels)))
          
  ; Random row list
  (defun fill-row-list (n pixels)
    (if (consp pixels)
        (cons (cons n (car pixels))
              (fill-row-list (+ n 1) (cdr pixels)))
        nil))
              
  ; Tests a legal case
  (check-expect (get-dimensions
                 (crop (make-bmp-tree 
                        (list (list 0 0 0 0 0 0 0 0 0 0 0 0
                                   0 0 0 0 0 0 3 0 0 0 3)
                              (list 0 0 (list 1 1 1)) 
                              (list 0 1 (list 2 2 2))
                              (list 0 2 (list 3 3 3)) 
                              (list 1 0 (list 4 4 4))
                              (list 1 1 (list 5 5 5)) 
                              (list 1 2 (list 0 0 0))
                              (list 2 0 (list 7 7 7)) 
                              (list 2 1 (list 8 8 8))
                              (list 2 2 (list 9 9 9))))
                       1 0 1 1))
                (cons 1 2))

  ; Tests a case in which a bmp-tree is not given  
  (check-expect (get-dimensions
                 (crop nil 1 0 1 1))
                nil)
  
  ; Tests a case in which the new dimensions are illegal,
  ; in this case firstRow > lastRow nad firstCol > lastCol.
  ; In this case, the tree is not cropped and the crop function
  ; returns the original tree.
  (check-expect (get-dimensions
                 (crop (make-bmp-tree 
                        (list (list 0 0 0 0 0 0 0 0 0 0 0 0
                                   0 0 0 0 0 0 3 0 0 0 3)
                              (list 0 0 (list 1 1 1)) 
                              (list 0 1 (list 2 2 2))
                              (list 0 2 (list 3 3 3)) 
                              (list 1 0 (list 4 4 4))
                              (list 1 1 (list 5 5 5)) 
                              (list 1 2 (list 0 0 0))
                              (list 2 0 (list 7 7 7)) 
                              (list 2 1 (list 8 8 8))
                              (list 2 2 (list 9 9 9))))
                       1 1 0 0))
                (cons 3 3))
  
  ; Verifies that trim-columns always returns the correct sized row.
  (defproperty trim-columns-returns-correct-sized-row-prp
    (colNum :value (random-between 1 25)
     firstCol :value (random-between 0 (- colNum 1))
     lastCol :value (random-between firstCol (- colNum 1))
     pixels :value (random-list-of (random-pixel) :size colNum)
     rowlist :value (fill-row-list 0 pixels))
    (equal (len (trim-columns rowlist firstCol lastCol))
           (+ (- lastCol firstCol) 1)))
     
  ; Verifies that trim-columns returns a row whose beginning and
  ; endng elements are at the given column bounds.
  (defproperty trim-columns-returns-correct-columns-prp
    (colNum :value (random-between 1 25)
     firstCol :value (random-between 0 (- colNum 1))
     lastCol :value (random-between firstCol (- colNum 1))
     pixels :value (random-list-of (random-pixel) :size colNum)
     rowlist :value (fill-row-list 0 pixels)
     newlist :value (trim-columns rowlist firstCol lastCol)) 
    (and (equal (cdar newlist) (cdr (nth firstCol rowlist)))  
         (equal (cdar (last newlist)) (cdr (nth lastCol rowlist)))))

  ; Verifies that trim-columns always returns a proper row-list.
  (defproperty trim-columns-returns-row-list-prp
    (colNum :value (random-between 1 25)
     firstCol :value (random-between 0 (- colNum 1))
     lastCol :value (random-between firstCol (- colNum 1))
     pixels :value (random-list-of (random-pixel) :size colNum)
     rowlist :value (fill-row-list 0 pixels)) 
    (row-list? (trim-columns rowlist firstCol lastCol)))
  
  ; Tests if the crop function returns the correct sized bitmap by 
  ; generating a random 25x25 bitmap, using the crop function to 
  ; change its dimensions, and then comparing the size of the new 
  ; tree to the randomized height and width.
  (defproperty crop-returns-correct-sized-bitmap-prp
    (height :value (random-between 1 25)
     width :value (random-between 1 25)
     lastRow :value (random-between 0 (- height 1))
     lastCol :value (random-between 0 (- width 1))
     firstRow :value (random-between 0 lastRow)
     firstCol :value (random-between 0 lastCol)
     bitmap   :value (random-bitmap height width))
    (equal (cons (+ (- lastRow firstRow) 1) 
                 (+ (- lastCol firstCol) 1))
           (get-dimensions (crop bitmap firstRow firstCol lastRow 
                                 lastCol))))

  ; Tests if the crop function returns the portion of the bitmap
  ; matching the specified pixel bounds by generating a random 25x25 
  ; bitmap, using the crop function to change its dimensions, and 
  ; then comparing the first pixel in the cropped bitmap with the
  ; lower bound pixel in the original bitmap and comparing the last
  ; pixel in the cropped image with the upper bound pixel in the
  ; original bitmap.
  (defproperty crop-returns-correct-subimage-prp
    (height :value (random-between 1 25)
     width :value (random-between 1 25)
     lastRow :value (random-between 0 (- height 1))
     lastCol :value (random-between 0 (- width 1))
     firstRow :value (random-between 0 lastRow)
     firstCol :value (random-between 0 lastCol)
     bitmap   :value (random-bitmap height width))
    (let* ((cropped (crop bitmap firstRow firstCol 
                          lastRow lastCol))
           (dimensions (get-dimensions cropped))
           (newHt (car dimensions))
           (newWd (cdr dimensions)))
      (and (equal (get-pixel-color bitmap firstRow firstCol)
                  (get-pixel-color cropped 0 0))
           (equal (get-pixel-color bitmap lastRow lastCol)
                  (get-pixel-color cropped (- newHt 1)
                                   (- newWd 1))))))
  
  ; Verifies that crop always returns a true bmp-tree given
  ; legal inputs.
  (defproperty crop-returns-true-bmp-tree-prp
    (height :value (random-between 1 25)
     width :value (random-between 1 25)
     lastRow :value (random-between 0 (- height 1))
     lastCol :value (random-between 0 (- width 1))
     firstRow :value (random-between 0 lastRow)
     firstCol :value (random-between 0 lastCol)
     bitmap   :value (random-bitmap height width))
    (true-bmp-tree? (crop bitmap firstRow firstCol
                          lastRow lastCol)))
  )

(link RTcrop (Mavltree Mbmptree Mdatagenerators Mcrop Tcrop))
(invoke RTcrop)